#define N 2   
#define M 6    /* full password length */
bit code[M]   

proctype proc (byte my_id, next_id, previous_id; chan to_next, from_previous, to_receiver){
	bit my_code[M] ;
	byte i = 0;
	byte j = 0;
	byte k = 0;
	byte m = 0;
/* declare more variables */

/* first getting the N bits belonging to this process from the global password */
	do
		:: i < N -> my_code[my_id*N+i] = code[my_id*N+i] ; i++
		:: i == N -> break
	od;

/* now the communication and result calculation begins ...*/
	do
		:: j < N -> to_next!my_code[my_id*N+j];
			from_previous?my_code[previous_id*N+j]; j++
		:: j == N -> break	
	od;
/* Put the last 2 code in each Proc */
	do
		:: k < N -> to_next!my_code[previous_id*N+k];
			from_previous?my_code[next_id*N+k]; k++
		:: k == N -> break
	od;
/* Save to Rcv */
	end1:
	do
		:: m < M -> end2: to_receiver!my_code[m]; m++
		:: m == M -> break
	od	
}

proctype receiver (chan from_A, from_B, from_C){
	bit my_code[M] ;
	byte i = 0;
	byte n = 0;	
/* declare more variables */
/* now the communication and result calculation begins */
		if
			:: from_A?my_code[i]; i++ -> 
				do
					:: i < M -> from_A?my_code[i]; i++
					:: i == M -> break
				od;
			:: from_B?my_code[i]; i++ ->
				do
					:: i< M -> from_B?my_code[i];i++
					:: i == M -> break
				od;
			:: from_C?my_code[i]; i++ ->
				do
					:: i< M -> from_C?my_code[i];i++
					:: i == M -> break
				od;
		fi;
		end3:
		do
			:: n < M
			-> assert( my_code[n]== code[n] )
			-> n++
			:: n == M
			-> break
		od
}
 
init { 
     chan  AtoB =  [2] of { bit };     /*message types for the channels may be extended in your solution !!! */
     chan  BtoC =  [2] of { bit }; 
     chan  CtoA =  [2] of { bit }; 
     chan  AtoR =  [2] of { bit }; 
     chan  BtoR =  [2] of { bit }; 
     chan  CtoR =  [2] of { bit }; 

	atomic{
		code[0] = 1; 
      	code[1] = 0;
      	code[2] = 1; 
      	code[3] = 1;
      	code[4] = 1; 
      	code[5] = 0;

     	run proc (0,1,2,AtoB,CtoA,AtoR);
     	run proc (1,2,0,BtoC,AtoB,BtoR);
     	run proc (2,0,1,CtoA,BtoC,CtoR);
     	run receiver(AtoR,BtoR,CtoR);
	}
}